\begin{tabbing}
(\=(AssertBY $\parallel$[]$\parallel$ $\geq$ 0  ((Reduce 0) \+
\\[0ex]CollapseTHEN ((Auto\_aux (first\_nat 1:n) ((first\_nat 
\-\\[0ex]2\=:n),(first\_nat 3:n)) (first\_tok :t) inil\_term)))$\cdot$) \+
\\[0ex]CollapseTHEN (InstConcl [$\lambda$$i$.
\-\\[0ex]if $i$ $\leq$z $\parallel$$L_{1}$$\parallel$ then $f_{1}$($i$) else $f$($i$ {-} $\parallel$$L_{1}$$\parallel$) fi ]))$\cdot$
\end{tabbing}